open util/ordering[Time]

sig Cap {
  auth: one Auth,
  opaque: one Opaque
}
fact { all disj c, c':Cap | c.opaque != c'.opaque }

sig Auth { }
sig Opaque { }


sig DNS{
	parent : DNS + DNSRoot,
	resolvesTo : set NetworkEndpoint
}{
// A DNS Label resolvesTo something
	some resolvesTo
}

one sig DNSRoot {}

fact dnsIsAcyclic {
	 all x: DNS | x !in x.^parent
//	 all x:dns-dnsRoot | some x.parent
}

abstract sig Principal {
// without the -HTTPClient the HTTPS check fails
	servers : set NetworkEndpoint,
	dnslabels : set DNS,
}

fact DNSIsDisjointAmongstPrincipals {
	all disj p1,p2 : Principal | (no (p1.dnslabels & p2.dnslabels)) and ( no (p1.servers & p2.servers)) 
//The servers disjointness is a problem for virtual hosts. We will replace it with disjoint amongst attackers and trusted people or something like that
}

// turn this on for intermediate checks
// run show {} for 6

sig Time {}

// Conservative assumption: Any raw data can contain (serialized) caps
sig Token { tokenCaps: set Cap }

// second.pre >= first.post
pred happensBeforeOrdering[first:Event,second:Event]{
	second.pre in first.post.*next
}

// shorter name
pred happensBefore[first:Event,second:Event]{
	second.pre in first.post.*next
}

fact Traces{
	all t:Time- last | one e:Event | e.pre=t and e.post=t.next
	all e:Event | e.post=e.pre.next
}


sig NetworkEndpoint{}

abstract sig Event {pre,post : Time} { }

abstract sig NetworkEvent extends Event {
    from: NetworkEndpoint,
    to: NetworkEndpoint
}

// we don't make HTTPServer abstract, it will be defined by the owner

abstract sig HTTPConformist extends NetworkEndpoint{}
sig HTTPServer extends HTTPConformist{}
abstract sig HTTPClient extends HTTPConformist{ 
  owner:WebPrincipal // owner of the HTTPClient process
}
sig Browser extends HTTPClient {
	trustedCA : set certificateAuthority
}
sig InternetExplorer extends Browser{}
sig InternetExplorer7 extends InternetExplorer{}
sig InternetExplorer8 extends InternetExplorer{}
sig Firefox extends Browser{}
sig Firefox3 extends Firefox {}
sig Safari extends Browser{}

abstract sig Method {}
one sig GET extends Method {}
one sig PUT  extends Method {}
one sig POST extends Method {}
one sig DELETE extends Method {}
one sig OPTIONS extends Method {}

fun safeMethods[]:set Method {
	GET+OPTIONS
}

abstract sig HTTPHeader { headerCaps: set Cap }
abstract sig HTTPResponseHeader extends HTTPHeader{} 
abstract sig HTTPRequestHeader extends HTTPHeader{}
abstract sig Status  {}
abstract sig RedirectionStatus extends Status {}

fact noOrphanedHeaders {
  all h:HTTPRequestHeader|some req:HTTPRequest|h in req.headers
  all h:HTTPResponseHeader|some resp:HTTPResponse|h in resp.headers
}

//////////////////
//////////////////
//////////////////

abstract sig HTTPEvent extends NetworkEvent { host : Origin }

sig URL {path:Path, host:Origin}

sig HTTPRequest extends HTTPEvent { 
  // host + path == url
  method: Method,
  path : Path,
  queryString : set attributeNameValuePair,  // URL query string parameters
  headers : set HTTPRequestHeader,
  body :  set Token
}

sig HTTPResponse extends HTTPEvent {
		statusCode : Status ,
		headers : set HTTPResponseHeader,
    body : set Token
}


// Browsers run a scriptContext
sig ScriptContext { 
	owner : Origin,
	location : Browser,
	transactions: set HTTPTransaction
}{
// Browsers are honest, they set the from correctly
	transactions.req.from = location
}


one sig c301,c302,c303,c304,c305,c306,c307 extends RedirectionStatus {}
one sig c200,c401 extends Status{}
sig location extends HTTPResponseHeader {targetOrigin : Origin, targetPath : Path}
// The name location above easily conflicts with other attributes and variables with the same name. 
// We should follow the convention of starting type names with a capital letter.
// Address this in later clean-up.

sig attributeNameValuePair { name: Token, value: Token}

sig LocationHeader extends HTTPResponseHeader {
  targetOrigin : Origin,
  targetPath : Path,
  params : set attributeNameValuePair  // URL request parameters
}

abstract sig RequestAPI // extends Event 
{ requestCaps: set Cap } 


sig HTTPTransaction {
	req : HTTPRequest,
	resp : lone HTTPResponse,
	cert : lone Certificate,
	cause : lone HTTPTransaction + RequestAPI
}{
	some resp implies {
		//response can come from anyone but HTTP needs to say it is from correct person and hosts are the same, so schema is same
		resp.host = req.host
		happensBeforeOrdering[req,resp]
	}

	req.host.schema = HTTPS implies some cert and some resp 
	some cert implies req.host.schema = HTTPS

}

fact CauseHappensBeforeConsequence  {
	all t1: HTTPTransaction | some (t1.cause) implies {
       (some t0:HTTPTransaction | (t0 in t1.cause and happensBeforeOrdering[t0.resp, t1.req]))  
       or (some r0:RequestAPI | (r0 in t1.cause ))
       // or (some r0:RequestAPI | (r0 in t1.cause and happensBeforeOrdering[r0, t1.req]))
    }
}

fun getTrans[e:HTTPEvent]:HTTPTransaction{
	(req+resp).e
}

fun getScriptContext[t:HTTPTransaction]:ScriptContext {
		transactions.t
}




fun getContextOf[request:HTTPRequest]:Origin {
	(transactions.(req.request)).owner
}

pred isCrossOriginRequest[request:HTTPRequest]{
		getContextOf[request].schema != request.host.schema or
		getContextOf[request].dnslabel != request.host.dnslabel
}

enum Schema{HTTP,HTTPS}
sig Path{}
sig INDEX,HOME,SENSITIVE, PUBLIC, LOGIN,LOGOUT,REDIRECT extends Path{}
sig PATH_TO_COMPROMISE extends SENSITIVE {}

sig Origin {
//	port: Port, 
	schema: Schema,
	dnslabel : DNS,
}


abstract sig certificateAuthority{}
one sig BADCA,GOODCA extends certificateAuthority{}

sig Certificate {
	ca : certificateAuthority,
	cn : DNS,
	ne : NetworkEndpoint
}{

	//GoodCAVerifiesNonTrivialDNSValues
	ca in GOODCA and cn.parent != DNSRoot implies 
			some p:Principal | {
				cn in p.dnslabels
				ne in p.servers
				ne in cn.resolvesTo
			}
}

/***********************

HTTP Facts

************************/


fact scriptContextsAreSane {
	all disj sc,sc':ScriptContext | no (sc.transactions & sc'.transactions)
	all t:HTTPTransaction | t.req.from in Browser implies t in ScriptContext.transactions
}


fact HTTPTransactionsAreSane {
	all disj t,t':HTTPTransaction | no (t.resp & t'.resp ) and no (t.req & t'.req)
}





/**************************** 

HTTPServer Definitions 

****************************/

one sig ACTIVEATTACKER extends Principal{}

//Passive Principals match their http / network parts
abstract sig PassivePrincipal extends Principal{}{
	servers in HTTPConformist
}

one sig PASSIVEATTACKER extends PassivePrincipal{}
sig WebPrincipal extends PassivePrincipal {
  httpClients : set HTTPClient
} { httpClients.owner = this }

//HTTPAdherent so that it can make requests too
one sig WEBATTACKER extends WebPrincipal{}

abstract sig NormalPrincipal extends WebPrincipal{} { 	dnslabels.resolvesTo in servers}
one sig GOOD extends NormalPrincipal{}
one sig SECURE extends NormalPrincipal{}

fact NonActiveFollowHTTPRules {
// Old rule was :
//	all t:HTTPTransaction | t.resp.from in HTTPServer implies t.req.host.server = t.resp.from
// We rewrite to say HTTPAdherents cant spoof from part ... here we don't say anything about principal
	all httpresponse:HTTPResponse | httpresponse.from in HTTPConformist implies httpresponse.from in httpresponse.host.dnslabel.resolvesTo
}

fact SecureIsHTTPSOnly {
// Add to this the fact that transaction schema is consistent
	all httpevent:HTTPEvent | httpevent.from in SECURE.servers implies httpevent.host.schema = HTTPS
//	STS Requirement : all sc : ScriptContext | some (getPrincipalFromOrigin[sc.owner] & SECURE ) implies sc.transactions.req.host.schema=HTTPS
}


fact NormalPrincipalsHaveNonTrivialDNSValues {
// Normal Principals don't mess around with trivial DNS values
   DNSRoot !in NormalPrincipal.dnslabels.parent
}

fact WebPrincipalsObeyTheHostHeader {
	all aResp:HTTPResponse | 
		let p = servers.(aResp.from) |
			p in WebPrincipal implies {
				//the host header a NormalPrincipal Sets is always with the DNSLabels it owns
				aResp.host.dnslabel in p.dnslabels
				// it also makes sure that the from server is the same one that the dnslabel resolvesTo
				aResp.from in aResp.host.dnslabel.resolvesTo

				//additionally it responds to some request and keep semantics similar to the way Browsers keep them
				some t:HTTPTransaction | t.resp = aResp and t.req.host.dnslabel = t.resp.host.dnslabel and t.req.host.schema = t.resp.host.schema
			}
}

fact NormalPrincipalsDontMakeRequests {
	no aReq:HTTPRequest | aReq.from in NormalPrincipal.servers 
}

fun smartClient[]:set Browser {
  Firefox3 + InternetExplorer8 
}

pred basicModelIsConsistent {
  some ScriptContext
  some t1:HTTPTransaction |{
    some (t1.req.from & Browser ) and
    some (t1.resp)
  }
}
run basicModelIsConsistent  for 8 but 3 HTTPResponse//, 3 HTTPRequest, 

///////////////////////////////////////////////////////////////////////////////
// from browserFacts.als

// This isn't quite right.  We might need a concept of a "pure" client that isn't also a server.
fact ClientsOnlyRequest {
	all ne:NetworkEvent | ne.from in HTTPClient implies ne in HTTPRequest
}

fact BrowsersTrustGoodCAOnly{
	Browser.trustedCA = GOODCA
}

pred correctHTTPSTransaction[t:HTTPTransaction] {
			t.req.host.schema = HTTPS
			t.cert.ca in (t.req.from).trustedCA
			t.cert.cn = t.resp.host.dnslabel
			t.cert.ne = t.resp.from 
}
// smartClients don't click through errors, others do
fact browserDropsBadlyCertifiedPackets {
	all t : ScriptContext.transactions | t.req.host.schema=HTTPS and 	t.req.from in smartClient implies correctHTTPSTransaction[t]
}

run show{} for 6 but exactly 6 Time

/*************************
*
*  Redirection Behaviour of Browsers
*
**************************/

pred sameOrigin[o1:Origin , o2:Origin]{ 
	o1.schema=o2.schema and
	o1.dnslabel = o2.dnslabel
}


fact BrowserRedirectionFact {
all first,second:HTTPTransaction | first=second.cause implies {
// you are either in the same scriptcontext or you are in no particular scriptcontext
			some sc :ScriptContext | first+second in sc.transactions or no ((first+second) & ScriptContext.transactions)
			//same from is implied by same ScriptContext
			some first.resp
			happensBeforeOrdering[first.resp,second.req]
//			some (second & (transactions.first).transactions) //the second is in the same scriptContext
			first.resp.statusCode in RedirectionStatus
			second.req.host =(first.resp.headers & location).targetOrigin
			second.req.path = (first.resp.headers & location).targetPath
			let redirRelation = (transactions.first).location -> first.resp.statusCode -> first.req.method -> second.req.method | 
					sameOrigin[first.req.host,second.req.host ] implies redirRelation in BrowserRedirectionBehaviour else redirRelation in CrossOriginBrowserRedirectionBehaviour
			}
}

fun CrossOriginBrowserRedirectionBehaviour [] : Browser -> RedirectionStatus -> Method -> Method {
	BrowserRedirectionBehaviour - ( InternetExplorer -> RedirectionStatus -> OPTIONS -> Method  +
		Firefox -> c307 -> OPTIONS -> Method  + Safari -> RedirectionStatus -> OPTIONS -> Method )
}

fun BrowserRedirectionBehaviour [] : Browser -> RedirectionStatus -> Method -> Method {
	Firefox->FirefoxRedirectionBehaviour
	+ Safari -> SafariRedirectionBehaviour 
	+ InternetExplorer -> IERedirectionBehaviour

}

fun FirefoxRedirectionBehaviour [] : RedirectionStatus->Method->Method {
	(c301 + c302 + c303) ->(GET+PUT+POST+DELETE + OPTIONS)->GET +
	c304->GET->GET +
	c307->( (GET+POST +PUT + DELETE  + OPTIONS) <: iden )
}

fun SafariRedirectionBehaviour [] : RedirectionStatus->Method->Method {
	(RedirectionStatus - c304) -> (GET+DELETE+PUT+POST+OPTIONS) -> GET
}

fun IERedirectionBehaviour [] : RedirectionStatus -> Method -> Method {
	c301-> GET -> GET + (c301+c302+c303)->POST -> GET + 
	(c301+c302+c303 + c307)->( (PUT+DELETE + OPTIONS) <: iden ) +
	c307 -> POST -> POST
}

///////////////////////////////////////////////////////////////////////////////
// from requestAPI

/************************************
* RequestAPI
*
************************************/

sig XMLHTTPRequest extends RequestAPI {	headers: set HTTPRequestHeader}

sig XMLHTTPRequest2 extends RequestAPI {
	headers: set HTTPRequestHeader
}

sig XDomainRequest extends RequestAPI {}

///////////////////////////////////////////////////////////////////////////////
// from CORS

/************************************
* CORS
*
************************************/
sig PreFlightRequest extends HTTPRequest {}{
	method = OPTIONS
	some headers & AccessControlRequestMethod
	// some headers & OriginHeader
	some headers & AccessControlRequestHeaders
}

fact PreFlightIsAlwaysCrossOrigin{
	all pfr:PreFlightRequest | isCrossOriginRequest[pfr]
}

abstract sig CORSResponseHeader extends HTTPResponseHeader{}
sig AccessControlAllowOrigin extends CORSResponseHeader {origin: Origin}
sig AccessControlAllowMethods extends CORSResponseHeader {allowedMethods : set Method}
sig AccessControlAllowHeaders extends CORSResponseHeader {allowedHeaders : set HTTPRequestHeader}
sig AccessControlMaxAge,AccessControlAllowCredentials extends CORSResponseHeader{}


abstract sig CORSRequestHeader extends HTTPRequestHeader{}
sig AccessControlRequestMethod extends CORSRequestHeader {requestedMethod : Method}
sig AccessControlRequestHeaders extends CORSRequestHeader {requestedHeaders : set HTTPRequestHeader}

run show {} for 6

/* Execution result:
Executing "Run show for 6"
   Solver=sat4j Bitwidth=4 MaxSeq=6 SkolemDepth=1 Symmetry=20
   32458 vars. 1798 primary vars. 65424 clauses. 52047ms.
   Instance found. Predicate is consistent. 201ms.
*/

///////////////////////////////////////////////////////////////////////////////
// from requestAPIFacts.als

fact XHRNoCrossOriginRequestOrRedirect{
	all t:ScriptContext.transactions |
		t.^cause in (XMLHTTPRequest+HTTPTransaction) implies not isCrossOriginRequest[t.req]
}

fact XHR2_CrossOrigin {
	all t:ScriptContext.transactions | 
		t.^cause in (XMLHTTPRequest2+HTTPTransaction) implies { 
						CORSPreFlightRequestTransaction[t] 
						or simpleCORSTransaction[t] 
						or complexCORSTransaction[t]
						or (not isCrossOriginRequest[t.req])
					}
}

pred simpleCORSTransaction[t:HTTPTransaction]{
		isCrossOriginRequest[t.req]
		t.cause in XMLHTTPRequest2 //As simple CORS Transaction don't redirect
		t.req.method in GET + POST
}
	
pred CORSPreFlightRequestTransaction[t:HTTPTransaction]{
	t.req in PreFlightRequest
    isCrossOriginRequest[t.req]
	t.cause in XMLHTTPRequest2
	//no redirects for CORSPreflight
	t.resp.statusCode in c301+c302+c303+c307 implies no t.(~cause)
}



//Remove all preflight request requirement in this .. add that to servers, that they make such type response only for a preflightRequest
pred complexCORSTransaction[t:HTTPTransaction]{
	t.req !in PreFlightRequest
	isCrossOriginRequest[t.req]
	t.cause in XMLHTTPRequest2 // no redirect allowed
	some t1:(transactions.t).transactions | {
		CORSPreFlightRequestTransaction[t1]
		t1.req.host = t.req.host
		t1.req.path = t.req.path		
		some (t.req.method & (t1.resp.headers & AccessControlAllowMethods).allowedMethods)
		some ((transactions.t).owner.dnslabel & (t1.resp.headers & AccessControlAllowOrigin).origin.dnslabel)
	}
	t.resp.statusCode in c301+c302+c303+c307 implies no t.(~cause)
}

fact XDROnlyDoesPostOrGet {
	all t:HTTPTransaction | t.cause in XDomainRequest implies {
			t.req.method in GET + POST
			t in (location.InternetExplorer).transactions
			not (t.req.host.schema = (transactions.t).owner.schema and t.req.host.dnslabel = (transactions.t).owner.dnslabel )
	}
}


fact XDRRedirect {
	all t:HTTPTransaction | t.cause in XDomainRequest implies {
			(t.^(~cause)).req.method=GET //all transactions caused by this other than itself
			some t.(~cause) implies  { //if there is a transaction caused by this
					(t.req.method=GET and t.resp.statusCode in c301+c302+c303+c307) or  
					(t.req.method=POST and t.resp.statusCode in c301+c302+c303)
			}
	}
}

// What about how the server opts into letting XDR tell the script context about the value of the response?

run show {} for 6

/*

Executing "Run show for 6"
   Solver=sat4j Bitwidth=4 MaxSeq=6 SkolemDepth=1 Symmetry=20
   99857 vars. 2158 primary vars. 207102 clauses. 56137ms.
   Instance found. Predicate is consistent. 1596ms.

*/
